This PR adds support for attaching attributes directly to structure fields, applying them to the generated projection functions.

Currently, attributes on structure fields are rejected with "Invalid attribute: Attributes cannot be added to fields", requiring users to
write separate attribute commands after the structure definition. This PR removes that restriction and applies field attributes to the corresponding projection declarations during structure elaboration.

Example:

-- Before:
structure Config where
  oldField : Nat
  normalize : String → String

attribute [deprecated "Use newField instead"] Config.oldField
attribute [simp] Config.normalize

-- After:
structure Config where
  @[deprecated "Use newField instead"] oldField : Nat
  @[simp] normalize : String → String

This also enables metadata-style attributes for downstream tooling, such as serialization frameworks:

structure User where
  @[json_rename "user_name"] userName : String
  @[json_rename "email_address"] email : String

The implementation is minimal, it removes the restriction in checkValidFieldModifier and applies attributes to projections in the structure finalization step using the existing Term.applyAttributes mechanism (similar to how docstrings are handled). No new storage or infrastructure was introduced.

Closes #13221